es:ES, l:IdLnk, e:E.
e':E
(e'':E.
(isrcv(e''))
 (sender(e'') = e)
 (lnk(e'') = l)
 (e'' c e' & loc(e') = destination(l)  Id)) 

latex

Definitions	ES, isrcv(e), E, sender(e), lnk(e), loc(e), kind(e), es_info(es), EOrderAxioms(E; pred?; info), P  Q, x:A. B(x), x:AB(x), P & Q, x:A  B(x), Id, e c e', <a, b>, IdLnk, s = t, b, x:A. B(x), t  T, (e < e'), es-pred?(es), sender(e), lnk(k), A c B, , P  Q, left + right, e < e', loc(e), destination(l), isrcv(k), kind(e)
Lemmas	rcv?-link, rcv?-kind, kind wf, isrcv wf, assert wf, ldst wf, loc wf, cless wf, lnk wf, sender wf